COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	report[f84,jmc]		To DARPA about recent work
C00046 ENDMK
C⊗;
report[f84,jmc]		To DARPA about recent work

Ron:
	Sorry this took so long.  It can be modified if its format
is unsuitable.

FORMAL REASONING AND COMMON LISP

	The formal reasoning group during 1984 included Professor John
McCarthy, Drs. Richard P. Gabriel, Paul Wieneke and Carolyn Talcott,
Professor Vladimir Lifschitz during the summer, Joseph Weening, and
Yoram Moses.

	McCarthy and Lifschitz worked on non-monotonic reasoning.  Gabriel
and Wieneke worked on Common Lisp and parallel Lisp.  McCarthy worked
on parallel Lisp also.  Carolyn Talcott worked on the foundations of
Lisp-like programming languages.  Weening worked on parallel execution
of Lisp.  Moses worked on the relation of knowledge and computation.
The work on these subjects is described in the following sections.

1. NON-MONOTONIC REASONING APPLIED TO COMMON SENSE

John McCarthy and Vladimir Lifschitz

	McCarthy's main work has been continuing research on non-monotonic
reasoning and its application to artificial intelligence.
(McCarthy 1980) describes the original work resulting in the circumscription
method of non-monotonic reasoning, and (McCarthy 1984) gives
an improved method and applies it to formalizing common sense knowledge.
While the details are in these documents here is a summary.

	An intelligent system, e.g. and intelligent robot, must somehow
express what it knows about the world --- about the relation between
the appearances it senses and the actual state of its environment,
about how the effects of actions and events depend on the situation
in which they occur, and about its own knowledge or lack thereof and
the location of knowledge in other intelligences as well as in documents
and computer files.  There are four used and proposed vehicles for expressing
this knowledge --- natural language, procedures, ad hoc data structures
whose meaning resides in how they are interpreted by program, and
 the languages of mathematical logic.

	While many have advocated it
from time to time, natural language has not been used as a vehicle
for expressing general knowledge.  Partly this because much basic
human knowledge about the effects of physical actions and how
to interpret observations is not expressed linguistically, i.e.
people can't tell you how they do it, and no-one has ever tried
to write it down.  Besides this, however, rules of inference
for natural language have never been formulated and may not
even exist.

	Most AI program combine building knowledge into program,
i.e. expressing it procedurally, and representing it in ad hoc
data structures that are used by the programs.  This works, but
has always to led to systems of limited capability that have
to be rewritten when major expansions are wanted.  Knowledge
expressed as procedures is not easily obtained by a program for
itself.  This knowledge is almost always built in by the programmer.
When systems of this kind are generalized, they become more and
more like logic based systems.

	Mixed systems are increasingly common.  One kind of mixture
interprets logical expressions procedurally as in Prolog.  Another
kind represents information by logical expressions but gets new
expressions from old ones by ad hoc procedures rather than by
logical deduction.  Both of these methods achieve solve particular
problems at the cost of specialization.

	Using logic directly was proposed in (McCarthy 1960), but
perhaps the idea can be considered to go back to Leibniz.  He
proposed that there be a logical language and that argument
be replaced by calculation in human affairs.  He was unsuccessful
in devising a logical language, not even getting as far as propositional
calculus which had to wait for George Boole, 150 years later.  We
skip the further history of logic, although it is interesting and even important
for understanding where we are today.

	(McCarthy 1960) proposed a program that would use common
sense knowledge expressed in mathematical logic sentences to decide
what actions would achieve the system's goals.  Many attempts have
been made by different people to carry out this plan, but they have
up to now been forced to compromise generality in order to get
programs that solve particular classes of problems.

	Formalized non-monotonic reasoning was first proposed in
the late 1970s in several forms by several people including McCarthy.
Logic is monotonic in the sense that a conclusion drawn from
a collection of premisses will still follow when the set of
premisses is extended by adding more sentences.  Humans often
draw conclusions that must be taken back when more facts are
obtained.  While this has been recognized for a long time, it wasn't
realized that such non-monotonic reasoning could benefit from
mathematical logical formalization or even that such formalization
was possible.  Formalization makes it possible for computers to
use non-monotonic reasoning and for AI researchers to design
systems that do it in a systematic way.

	(McCarthy 1984) applies a new version of the circumscription
method to handling inheritance hierarchies with exceptions and
to solving the frame problem that afflicts planning systems.

McCarthy, John (1960): "Programs with Common Sense," in Proceedings of the
Teddington Conference on the Mechanization of Thought Processes, Her Majesty's
Stationery Office, London.

McCarthy, John (1980): 
"Circumscription - A Form of Non-Monotonic Reasoning", Artificial
Intelligence, Volume 13, Numbers 1,2, April.

McCarthy, John (1984):
"Applications of Circumscription to Formalizing Common Sense Knowledge".
This is has been accepted by the 1984 AAAI
conference on non-monotonic reasoning, which will not have a proceedings
and is being submitted for publication to Artificial Intelligence.

	Vladimir Lifschitz studied the mathematical properties of
circumscription.  He proved metamathematical results that can be sometimes
used for expressing the result of circumscription by first order formulas
and gave an interpretation of the unique names hypothesis in terms of
circumscription. These results are discussed in his paper, "Some Results
on Circumscription", presebted at the Non-Monotonic Reasoning Workshop in
New Paltz, October 17-19, 1984.


2. COMMON LISP AND QLAMBDA

Richard Gabriel, Paul Wieneke and John McCarthy

Qlambda

:  Overview

The Qlambda project was undertaken as part of the Common Lisp work at Stanford
and also as part of the feasibility study for the Advanced Architectures
Project at HPP. It's goal is to extend Common Lisp by adding parallel processing
constructs.

:  Objectives

Qlambda is an extension of Common Lisp which provides multi-processing 
capabilities. Qlambda supports a variety of parallel programming styles,
including parallel argument evaluation and message-passing. It is designed
to be implementable on a variety of multi-processor architectures.

:  Approach

The approach has been to write a detailed simulator for Qlambda to
simulate behavior of Qlambda programs on a multi-cpu, shared-address-space
computer. With this simulator it has been possible to write a number
of programs in Qlambda and explore the speedups attainable under varying machine
characteristic parameters.

:  Current Status

The basic Qlambda extensions have been defined and are available in the
report ``Queue-based Multi-processing Lisp,'' by Richard P. Gabriel and
John McCarthy, available as a Stanford University Computer Science Report.
The simulator runs in MacLisp under TOPS-20 and in Common Lisp on the
Symbolics 3600.

Several programming techniques have been defined and demonstrated in Qlambda.
These techniques will be described later.

: Important Contributions

The most important contributions of the Qlambda project have been to define
parallel programming techniques. There have been two major techniques
explored: software pipelining and geometric control structures.

Software pipelining is breaking a serial program into stages and mounting
the stages on different processors. The technique includes mechanisms for
maintaining global variables among the stages. That is, if the original
program contained global variables which were used to pass information
between subsequent calls to the program, it is still possible to pipeline the
program and achieve a significant speedup. This technique is useful for
parallelizing globally-shared data structures by streaming update and
access requests through the code which maintains the data structures
in question.

Geometric control structures are  a technique for matching the `architecture'
of a problem solution to the architecture of the underlying machine.
Suppose that the problem solution calls for a hexagonal grid of processors
where each processor talks to six neighbors. A geometric control structure
is a hexagonal data structure where each node in the data structure is a
process (rather than a processor), and processes communicate with
other processes along the data-structure-defined paths to its six neighbors.

If a data structure containing processes can be mapped onto a physical
multi-processor so that the lines of communication defined by the data
structure map onto lines of communication defined by the architecture,
then the running speed of the solution program will be good.  And even on
general multi-processors which do not match the data structure well there
will usually be significant speedup.

We sometimes refer to geometric control structures as `soft architectures.'
The key idea behind this technique is that it allows the programmer to
solve his problem in an architecture well-suited to his problem and its
solution.

Portable Common Lisp

:  Overview

This project is to provide a portable Common Lisp implementation available
to DARPA contractors. The key to the project is to develop a high-quality 
Lisp compiler which can be ported easily to various machines. Because
Common Lisp is the prefered Lisp for Strategic Computing work, the availability
of Common Lisp on a variety of machines is essential.

:  Objectives

The first objective of the project is a Common Lisp compiler. This compiler
is to be largely table-driven or to have relatively small parts that are
machine-dependent. The second objective is to provide a Lisp-in-Lisp-style
Lisp implementation, which is then compiled on the various machines.

In addition, there is a corpus of code written in Common Lisp, which could
be useful to several projects, and which exists at particular sites. A second
goal of this work is to create a library of such useful programs along with
good documentation.

:  Approach

The approach is to start with the ideas in the S-1 Lisp, especially the compiler,
and to build a subset of Common Lisp for the SUN II workstation. This is a
popular and fairly powerful workstation. The subset is to be small enough to
run well on a SUN workstation with a small physical memory and perhaps a small
available address space. That is, the implementation is geared towards being 
usable on a mobile robot with a small MC68000-based machine on-board.

There is a problem with this approach, which is that there remains a significant
amount of machine-dependent code to be written on each port, even though the
its fraction of the total amount of code in the implementation is quite small.

:  Current Status

Currently there is a subset of Common Lisp that runs on the SUN II under the
V kernel, a Stanford operating system similar to Unix. The code is available
on magnetic tape, and several copies have been sent to various institutions.


3. FOUNDATIONS OF LISP-LIKE PROGRAMMING LANGUAGES
Carolyn Talcott

Talcott has continued work on Rum, which a theory of 
intensional and extensional aspects of the
side-effect free fragment of Lisp-type symbolic computation.
The goals of this work include obtaining a better understanding
of the mathematical properties of computations that can create
and apply higher type objects.  In Rum there are two classes
of higher type object: pfns, which are descriptions of partial functions
and continuations, which describe
how a computation is to continue when the current subcomputation returns a
value.
Pfns are analogs to closures as introduced by Landin [1] and implemented in 
Scheme [3].
Continuations are analogs to the J operator of Landin [2] and to the continuations
bound by the CATCH construct of Scheme.

In addition to pfns and continuations, the basic model includes forms and 
environments.  Forms are symbolic expressions describing computations
and environments are finite maps which assign values to free symbols in forms.  
Computation trees and sequences give the structure of computations 
described by forms.  These structures provide the basis for expressing
intensional properties of programs - such as counting the number of
conses,  counting the number of pfn applications, or measuring the
maximal stack depth required.  They also serve as the
basis for program transformations that map a program into one that
computes some property of the computation it describes -
thus transforming intensional properties of one program into extensional
properties of another.
Evalutation and subcomputation are derived from the computation structures
and provide the basis for treating extensional aspects - properites
of the ``function computed'' by a program.

The main results are:

() Two basic theorems about the computation relations
are the recursion theorem and a computation induction theorem.
The recursion theorem gives a recursion pfn that computes
a fixed point of pfns that compute functionals and thus provides
a means of definition by recursion.  Computation induction
expresses the fact that for computations which return a value,
the sub-computation relation is well-founded.

() A notion of comparison relation is introduced for tree \RUM! that includes
include both approximation relations (with respect to definedness)
and equivalence relations.
Each comparison relation corresponds to forgetting selected details of computation,
while preserving the evaluation and application structure.
Methods are developed for construction of comparison relations
and for proving properties of particular comparisons.
There is a maximal approximation relation, Xlt.  The intersection
of this relation with its inverse, Xeq is the maximal equivalence relation.
Two key theorems about these relations are (i) Xlt and Xeq are
extensional and (ii) the recursion pfn computes the least
fixed point with respect to Xlt.  Extensionality of Xlt means
that for any pair of pfns,
p0 and p1, p0 approximates p1 iff p0 applied to any
to any argument v approximates p1 applied to v.
Thus pfns describe partial functions on Xeq-equivalence
classes of the computation domain, and two pfns are equivalent
iff they describe the same partial function.
There is a rich hierarchy
of comparisons between equality and the maximal relations.
For example, forms related  by distribution of application
over conditional 

              f(if(p(x),x,y)) R if(p(x),f(x),f(y))

and by distribution of conditional over conditional 

if(if(p(x),q(x),r(x)),g(x),h(x)) R if(p(x),if(q(x),f(x),g(x)),if(r(x),f(x),g(x)))

give rise to equivalences
where related forms describe computation trees
with the same number of nodes of each sort, but 
different subcomputation structures.
The theory of comparison relations provides concepts and tools
useful in developing a theory of program specifications and
transformations.

() Notions of Rum machine structure and morphism are introduced.
A machine structure has states and a step relation, with states naturally
generated from a class of symbolic descriptions.
A morphism, M maps states s of the source machine  A
to states M(s) of the target machine B in a manner that carries 
the step relation Step{A} of the source machine to steps Step{B} of the
target machine.   That is,

  s0  Step{A} s1 iff M(s0) Step{B} M(s1)

Rum computation has a natural machine structure RM.
A machine structure is defined on the tree fragment based on 
sequential descriptions whose computaton trees
have a single main branch such that the value of the computation
is the value at the leaf of the main branch.
The main theorem is the existence of a compiling morphism
from RM to this sequential fragment.
This morphism serves as a paradigm for compiling and for proving properties of
compilers.  It makes precise the relation between closures and continuations
and  corresponds to the normal form theorem of
recursion theory.
 
() Working in Rum, a variety of examples are given 
to illustrate its potential applications and to demonstrate the
adequacy of the theory.  In particular we formulate and prove
the correctness of the following programs

-- a pattern matcher that uses closures to implement
backtracking in a search for all matches of an object to a pattern

-- a  program that uses continuations in order
to avoid unnecessary work in computing products represented as trees
with numbers at the leaves.  If a zero is encountered
it is returned directly to the caller 
rather than passing the information back in the normal fashion
to be rechecked at every level. 
This corresponds to the use of Catch and Throw in Lisp.





References:

[1]  
Landin,P.J.[1964]
The Mechanical Evaluation of Expressions
Computer Journal 6
pp. 308-320 

[2]
Landin,P.J.[1965]
A Correspondence Between ALGOL60 and Church's Lambda Notation
CACM 8 
pp. 89-101, 158-165. 

[3]
Steele, G.L., Sussman, G.J.[1975]
SCHEME, and Interpreter for Extended Lambda Calculus,
MIT AI Memo 349 (December 1975)

4. PARALLEL EXECUTION OF LISP PROGRAMS
Joseph Weening

Weening is pursuing his dissertation work in the study of parallel execution
of Lisp programs.  This includes a study of machine architectural features
appropriate for symbolic programming, as well as the problem of extracting
parallelism from sequentially-presented Lisp programs.  The queue-based
approach, in which assignment of processors to processes is decided as the
program is running, is assumed.

Architectural considerations take place in deciding how to efficiently
implement the basic constructs of Qlambda [1] or other dialects of parallel
Lisp, such as Multilisp [2].  Appropriate primitives provided in hardware
can greatly improve the performance of process waiting and access to shared
variables, which are essential activities in the queue-based approach.  The
Denelcor HEP [3] is an example of an architecture which provides the basis
for efficient process management.  (Other features of the HEP, such as its
read-only local program memory, make the implementation of Lisp somewhat
problematic.)

Extraction of parallelism involves studying the potential side effects of
a program, and deciding which parts may safely be executed on separate
processors without affecting the program's results.  Once this is done,
there remains the problem of deciding when it is actually beneficial to
execute part of a program in parallel.

[1] Gabriel, R.P., McCarthy, J., "Queue-based Multi-processing Lisp", 1984
ACM Symposium on Lisp and Functional Programming.

[2] Halstead, R.H., "Implementation of Multilisp: Lisp on a Multiprocessor",
1984 ACM Symposium on Lisp and Functional Programming.

[3] Smith, B.J., "A Pipelined, Shared Resource MIMD Computer", Proceedings
of the International Conference on Parallel Processors, 1978.

5. THE RELATION BETWEEN KNOWLEDGE AND COMPUTING
Yoram Moses

Yoram Moses is currently investigating the relationship between knowledge 
and computing. A previous work of his under this grant, dealing with
representation schemes and the expressibility of first order logic 
has just appeared in press as a paper titled ``On the encoding of 
relations by graphs'', in the SIAM Journal of Algebraic and Discrete 
methods, Vol. 5, No. 4, December 1984.

In his current work on knowledge, Moses is investigating both the 
formal aspects involved in developing Logics of Knowledge and 
Ignorance, and the less formal aspects of the relationship between 
knowledge and action in Artificial Intelligence and distributed 
computing. He is trying to characterize what states of knowledge are 
necessary for successfull cooperation of intelligent agents, and 
relating that to an analysis of what states of knowledge are 
practically attainable in communication between robots or computers 
in general. Among other things, this work suggests that a theory of
knowledge generalizing the well known theory of information is needed
as an appropriate framework in which to address the problems of 
cooperation in a society of intelligent agents, or in a distributed 
system. The following paragraphs briefly outline the work done in a 
number of papers Moses is currently writing, or has published in 
conferences and workshops. 

The paper ``Knowledge and common knowledge in distributed environments'' 
presents a number of well known puzzles regarding agents' actions in 
a situations in which there is interdependence between their actions. 
A hierarchy of states of knowledge that a group may be in is defined, 
and we describe how the state of knowledge called ``common knowledge'' 
is a necessary precondition for the ssccessful solution of these puzzles. 
It is then shown that common knowledge is an inherent part of agreements, 
and a necessary part of certain cases of coordinated action. We show 
that if the communication channels between agents are imperfect, in the 
sense that messages are not guaranteed to be delivered, or in the sense 
that there is a doubt as to precisely messages are delivered, common 
knowedge cannot truly be attained. In practice, literally all channels 
of communication are imperfect in one of these senses.
We define a variety of approximations to the notion of common knowledge, 
and discuss the extent and conditions fr them to act as ``worthy 
substitutes'' for common knowledge in distributed action. This paper 
appeared in the 3rd Annual Symposium on the Principles of Distributed 
Computing, held in Vancouver in August 1984, and has generated interest 
both in the distributed computing field and in the AI. 
This paper is joint with Joe Halpern of IBM San Jose.

A preliminary version of the paper ``Towards a theory of knowledge and 
ignorance'' was presented at the AAAI Workshop on Nonmonotonic Logic 
in New York in October 1984. It deals with the basic question of how 
an intelligent agent that is fully aware of the facts in his knowledge 
base can determine what facts he is ignorant of. Another way of stating
this is determining what ``knowing only p'' for a single formula p 
representing the information in the agent's knowledge base means. 
This problem has been identified by McCarthy and others as a fundamental 
question in the logic of knowledge. Konolige [1] and Moore [2] treat related
problems. A major problem in this work is demonstrating that a solution 
you come up with is in fact the right one. We take four different 
approaches to the solution: some ssmantically based, some syntatctically 
based, one an algorithm that solves the problem. In each one we find that 
there seems to be a natural solution for some well behaved ``honest'' 
formulas, but there are problematic formulas for which no such solution 
exists. We show that the classes of problematic formulas in all cases 
coincide, and that for an ``honest'' formula, all approaches give us the 
same answer. Thus, we have a robust notion of what ``knowing only p'' 
means. We also argue that ``dishonest'' formulas cannot truly represent 
all the information in a knowledge base. This work deals with the 
propositional modal logic of a single knower. We are in the process of 
extending it to the interesting case of mny knowers, and hope to solve 
the first order case too. This work is also joint with Joe Halpern of 
IBM San Jose. 

The paper ``A guide to the modal logics of knowledge and belief'' is an 
introduction to the formal aspects of its subject. It describes how 
possible-worlds semantics capture the notion of knowledge and belief, 
introduces the reader to the notion of Kripke structures as a possible-worlds 
formalism, and proves some of the basic well known properties of the 
resulting models for knowledge and belief. It then goes on to present 
efficient decision procedures for a variety of logics of knowledge, 
generalizing some results of Ladner [3], and proving some new results. 
The result is contrary to prevalent opinions in some circles, that claim  
that the modal approach to logics of knowledge is computationally 
intractable. This work, too, is joint with Joe Halpern. 

In the well known ``cheating wives'' puzzle, there is subtle interaction 
between agents' knwoledge and their actions. The puzzle opens with a 
``public'' statement that makes a number of facts common knowledge.
Artificial agents communicate via signals and messages, and it is not 
aways possible to perform ``public announcements'' in that setting.
The paper ``Cheating husbands and other stories: a case analysis of 
knowledge and action'', in preparation, is an analysis of how the states 
of knowledge arising from different modes of communication affect the 
success of the actions taken by intelligent agents in a society. 
Essentially, we look at variants of the cheating wives puzzle in which 
the announcement is delivered by a messenger rather than via a public 
announcement. Surprisingly, in many cases this denies the possibility 
of a successful solution to the puzzle. This work is joint with Danny 
Dolev of the Hebrew University, and with Joe Halpern from IBM San Jose. 

The paper ``Knowledge and common knowledge in Byzantine environments'' 
is a sequel to the ``distributed environments'' paper mentioned above. 
It deals with the characterization of the facts that can possibly 
become known in different modes of communication, and deals with the 
interesting case of characterizing the states of knowledge arising 
from messages that are received in societies that include faulty agents, 
liars etc. By proving a general theorem about the conditions required 
for obtaining common knowledge in such circumstances, we generalize 
a large number of known lower bounds, and demonstrate that the basic 
reason for them is in the inherent uncertainties in information 
distributed amongst agents that are potential liars. 
This paper is in preparation, and is joint with Cynthia Dwork of MIT.

References

\item{HM1} J.\ Y.\ Halpern and Y.\ Moses, Knowledge and common knowledge in
a distributed environment, {\it Proceedings of the 3rd ACM
Symposium on Principles of Distributed Computing}, 1984, pp.\ 50--61.
 
\item{HM2} J.\ Y.\ Halpern and Y.\ Moses, A guide to modal logics of knowledge,
to appear as an IBM RJ, 1984.
 
[1] K. Konolige, Circumscriptive ignorance,
    Conference Proceedings of AAAI--82, pp. 202--204.
 
[2] R. C. Moore, Semantical considerations on nonmonotonic logic,
    SRI International Technical Note 284, 1983.

[3] R. E. Ladner, The computational complexity of provability in
    systems of modal propositional logic,
    Siam J. Computing, Vol. 6, No. 3, 1977, pp. 467--480.